COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Brotz's thesis
C00008 ENDMK
C⊗;
Brotz's thesis

Dear Don,

Sorry, I was the one who misparsed! It occurred  to me that your note
was asking about Brotz's thesis in its entirety, and you'd only typed
the first two words of the title.

His thesis is interesting for its day, but has little for us now.  It
contained a small  set of axioms about elem. group  theory, and would
be  fed a theorem to prove (by a  human user).  The program then used
resolution to  prove that  theorem.   The "heuristic..."  came in  as
guidance for the  resolution proof.  Thus a  heuristic might exist in
his system that said  "try to elimiate the  least simple disjunct  in
the most  simple non-unit wff",  but when you  dig into the  code you
find  that "simplicity" is  defined as  the Lisp function  Count (the
fewer list cells, the simpler).

The problems are that he insisted on having the system prove theorems
fed  by  humans  (thus  the  machine  had  no  supporting  basis  for
understanding  and  wanting  and believing  the  theorem),  he relied
mainly on resolution, he had  only a few heuristics (all  very weak),
he insisted on  starting from the axioms each time  a new theorem was
to be fed in  (no gradual accumulation of  knowledge or expertise  or
memory of past theorems or memory of past  proofs). I'm not sure, but
I  believe he (and his  committee) were somewhat  disappointed by the
results   (only   special-case   improvement   over   "non-heuristic"
thm-provers).

I read  the thesis two  years ago,  and I don't  have my notes  right
here.   There is  the possibility that  I am  confusing this somewhat
with the theses of Kling and King.  When I find my notes (or remember
something else) I'll send you another message.

Regards,
Doug